es:event_system{i:l}, e,e':es-E(es).
es-locl(es; e; e')  sqequal([e, e']; append([e, es-pred(es; e')]; cons(e'; []))) 

latex

Definitions	x:A. B(x), P  Q, [e, e'], filter(P; l), before(e), t  T, Y, if b then t else f fi , tt, ff, prop{i:l}, reduce(f; k; as), es-le(es; e; e'), P  Q, , A, P  Q, P  Q, Unit, False, P  Q,
Lemmas	filter append, es-ble wf, es-before wf, es-pred wf, es-locl-iff, es-first wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, es-locl wf, es-E wf, event system wf, assert-es-ble